@UlfNorell Ouch, unification issues really make things tedious..

It's a little surprising that it's that much worse than the ultra-polymorphism version.

That's a nice idea! Can we use a tactic argument to default the first level mapping to id to solve the unification issues? If that works the overhead is contained in the class definitions (Functor, etc.) where you have to manually pass the first level mapping correctly and then all the places where you want to have a different first mapping.